We investigate the power of non-determinism in purely functional programminglanguages with higher-order types. Specifically, we consider cons-free programsof varying data orders, equipped with explicit non-deterministic choice.Cons-freeness roughly means that data constructors cannot occur in functionbodies and all manipulation of storage space thus has to happen indirectlyusing the call stack. While cons-free programs have previously been used by several authors tocharacterise complexity classes, the work on non-deterministic programs hasalmost exclusively considered programs of data order 0. Previous work has shownthat adding explicit non-determinism to cons-free programs taking data of order0 does not increase expressivity; we prove that this - dramatically - is notthe case for higher data orders: adding non-determinism to programs with dataorder at least 1 allows for a characterisation of the entire class ofelementary-time decidable sets. Finally we show how, even with non-deterministic choice, the originalhierarchy of characterisations is restored by imposing different restrictions.
展开▼
